#ifndef QPF_H
#define QPF_H

#include "base/aig.h"
#include "Proof.h"
#include "SolverTypes.h"
#include "vec.h"
#include <vector>

using std::vector;

typedef MinisatProof::Lit plit_t;
typedef MinisatProof::vec< MinisatProof::Lit > cls_t;


class Clause : public cls_t
{
   friend class QProof;
   friend class report_cls;

   vector<Clause * > out;
   plit_t   x;
   AigLit   itp;

   public:

   Clause * in[2];
   mutable uint8_t  mrk; // traverse and use in shorten 

   private:
   uint8_t          del; // means the clause is deleted 


   void change_input( Clause * from , Clause * to );
   void remove_output( Clause * t);
   
   void remove(); // soft delete
   void replace( Clause * t );
   bool slim( unsigned * lut );

   public:
   Clause():mrk(0),del(0){ in[0] = in[1] = NULL; }
   Clause( bool A ):mrk(0),del(0){ in[0] = in[1] = NULL; if(A==false)in[1]=this;}
   Clause( Clause * a , Clause * b , plit_t _x , unsigned * lut);

   bool isLeaf()const{return in[0] ==NULL;}
   bool isA()const{ assert(isLeaf());  return in[1] == NULL ; }

   void interpolant( StrashAIG & aig , int * base );
   bool inorder( const unsigned * lvl )const;
   void plot( std::ostream & out  )const;
   bool check_resolve( )const;
   bool check_connect( )const;
   
   // static pool 
   static vector<Clause * > DEL_BOX;
   static void remove_remove();

};

class QProof : virtual public MinisatProof::ProofTraverser
{
   vector<Clause * >    _cls;
   unsigned *           _lut;
   unsigned *           _lvl;

   Clause *             _root;

   Clause *resolve( Clause *  a , Clause * b , plit_t x );

   void swap_cls( Clause * c );
   void swap_cls( Clause * a_b , Clause * a_nb , Clause * na , Clause * a , Clause * z , plit_t la , plit_t lb );
   void shorten( Clause * c );

   vector< Clause * >   _stand_area;

   public:
   
   virtual ~QProof();
   void interpolant( StrashAIG & ckt , int * base );

   // init 
   void init( unsigned n );
   void set_lvl( unsigned n , unsigned l ){ _lvl[ n ] = l ;}

   // proof
   virtual void root   (const cls_t & c , uint8_t x );
   virtual void chain  (const MinisatProof::vec<int> & cs, const cls_t & xs);
   virtual void done  ();

   void swap_cls_by_propagate();
   void swap_cls_by_iterate();
   void report()const;
   void plot( const char * file )const;

   void check_resolve()const;
   void check_inorder()const;
   void check_connect()const;

};


#endif
